Ackermann set theory

Ackermann set theory is a version of axiomatic set theory proposed by Wilhelm Ackermann in 1956.

Contents

The language

Ackermann set theory is formulated in first-order logic. The language L_A consists of one binary relation \in and one constant V (Ackermann used a predicate M instead). We will write x \in y for \in(x,y). The intended interpretation of x \in y is that the object x is in the class y. The intended interpretation of V is the class of all sets.

The axioms

The axioms of Ackermann set theory, collectively referred to as A, consists of the universal closure of the following formulas in the language L_A

1) Axiom of extensionality:

\forall x \forall y ( \forall z (z \in x \leftrightarrow z \in y) \rightarrow x = y).

2) Class construction axiom schema: Let F(y,z_1, \dots, z_n) be any formula which does not contain the variable x free.

\forall y (F(y, z_1, \dots, z_n) \rightarrow y \in V) \rightarrow \exists x \forall y (y \in x \leftrightarrow F(y,z_1, \dots, z_n) )

3) Reflection axiom schema: Let F(y,z_1, \dots, z_n) be any formula which does not contain the constant symbol V or the variable x free. If z_1, \dots, z_n \in V then

\forall y (F(y, z_1, \dots, z_n) \rightarrow y \in V) \rightarrow \exists x (x \in V \land \forall y (y \in x \leftrightarrow F(y, z_1, \dots, z_n))).

4) Completeness axioms for V

x \in y \land y \in V \rightarrow x \in V
x \subseteq y \land y \in V \rightarrow x \in V.

5) Axiom of regularity for sets:

x \in V \land \exists y ( y \in x) \rightarrow \exists y ( y \in x \land \lnot \exists z (z \in y \land z \in x)).

Relation to Zermelo–Fraenkel set theory

Let F be a first-order formula in the language L_\in = \{\in\} (so F does not contain the constant V). Define the "restriction of F to the universe of sets" (denoted F^V) to be the formula which is obtained by recursively replacing all sub-formulas of F of the form \forall x G(x,y_1\dots, y_n) with \forall x (x \in V \rightarrow G(x,y_1\dots, y_n)) and all sub-formulas of the form \exists x G(x,y_1\dots, y_n) with \exists x (x \in V \land G(x,y_1\dots, y_n)).

In 1959 Azriel Levy proved that if F is a formula of L_\in and A proves F^V, then ZF proves F

In 1970 William Reinhardt proved that if F is a formula of L_\in and ZF proves F, then A proves F^V.

See also

References